Nuprl Definition : reverse
11,40
postcript
pdf
rev(
as
) == rec-case(
as
) of [] => [] |
a
::
as'
=>
.rev(
as'
) @ [
a
]
clarification:
rev(
as
) == rec-case(
as
) of [] => [] |
a
::
as'
=>
.rev(
as'
) @ [
a
/ []]
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
as
@
bs
,
f
(
a
)
,
[
car
/
cdr
]
,
[]
FDL editor aliases
reverse
origin
x.A(x)x.A(x)